COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00009 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂AIL Colonel David Russell↓Office of Information Processing Techniques
↓Defense Advanced Research Projects Agency
↓1400 Wilson Boulevard
↓Arlington, Virginia∞

Dear Dave:

	This letter concerns the program synthesis part of our proposal
written by Zohar Manna.  In my opinion, this new approach to the problem
is more promising than our previous program synthesis work embodied in the
PSI project.  The advantage, both from a basic research and a practical
point of view, is that it is based on sound mathematical approach to
specifying the program to be synthesized.  The specifications of the
program are distinguished from the program itself by the fact that the
while the specifications determine the input-output relations of the
program, they are not necessarily or even usually computable in themselves.
In Manna's view, which I share, this is how the state
of mind of someone who knows what the program is to accomplish differs
from the state of mind of someone who knows how to accomplish it.
From this point of view, program synthesis consists of transforming
this non-computable input-output relation into one which can be
efficiently computed, and Manna's proposal presents many ideas for
accomplishing this by a combination of human effort and automatic
computation.

	While Manna published his first paper on program synthesis
in 1971, most of his work in the area has taken place since he returned
to Stanford in 1975.

	PSI, on the other hand, is based on the idea of extracting
the specifications of a program from a man-machine dialog.  Unfortunately,
this project has never achieved a clear idea of what the specifications
are that are to be extracted.  Moreover, the techniques for man-machine
dialog are not really well-developed.

	If this change in direction were a purely internal matter
at Stanford, there would be no need for a letter apart from the
proposal itself.  However, the following facts complicate matters:

	1. Cordell Green is leaving Stanford, because the Computer
Science Department decided not to recommend his promotion to tenure.
In part this is because the Department and its outside referees
did not think that the PSI work, which has been his main work
over the last few years, made a clear case for tenure.  Almost certainly,
if the University rules permitted it, the Department would have
temporized and waited one or two years longer to see if PSI
would eventually succeed in impressing ourselves and the computer
science community internationally.  However, six years, somewhat
extended by leaves of absence, is all the time allowed.  A professor
must be given tenure or asked to go elsewhere after that time.

	2. On the other hand, the Department recommended that Manna
be appointed Professor of Computer Science, and this recommendation
has been approved by the School of Humanities and Science and is
now before the Provost.  (Recommendations that get this far are
almost always approved by the Board of Trustees).  The letters
we received from outside referees asked to compare Manna with
the leaders in the field were outstanding.  These letters mainly
considered his work in program verification; the program synthesis
work is too new.
These appointments were not directly competitive; the Department could
have recommended both, since we have the slots.

	3. I worry about asking ARPA to accept this change of direction
in our program synthesis work, because you may think that we
have no justification for it beyond our convenience given the change
in personnel.
Moreover, when I visited ARPA in April, Bill Carlson told me that he
considered the Manna work (I suppose on verification not synthesis)
as auxiliary to the work of Dave Luckham, and this is not the view
we would like you to take.

	This redirection of our synthesis work involves complex
scientific issues which you may not have time to give the attention
they require.
Moreover, you may worry about the possibility that the Stanford
Artificial Intelligence Laboratory and the Stanford Computer
Science Department have a conflict of interest in the matter.
If this is so, let me recommend that you obtain
leading people in the field of computer science as
outside consultants - choosing no-one from Stanford, since Stanford
has already committed itself.

.sgn